COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Making the closed world assumption explicit and "going down"
C00003 ENDMK
C⊗;
Making the closed world assumption explicit and "going down"

∀x.(isflight(psa,x) ≡ x ε database(psa))

"x is a PSA flight if and only if this fact is in the PSA database".

∀x.(x ε DB ⊃ true x)

∀x.(P(x) ⊃ (true x ≡ conseq(DB, x))

conseq(DB,x) ≡ ∃p.(isproof(p,x) ∧ ∀a.(assumption(a,p) ⊃ a ε DB)

more simply

∀x.(Q(x) ⊃ (true x ≡ x ε DB))